COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	book[e84,jmc]		Notes for modifying McCarthy and Talcott
C00009 00003	section on ekl and/or Boyer-Moore
C00010 00004	Outlines:
C00011 ENDMK
C⊗;
book[e84,jmc]		Notes for modifying McCarthy and Talcott

Notes based on version pubbed Sept. 15, 1980

page
ii
Many assertions about pure LISP programs were proved using Richard
Weyhrauch's (197x) FOL interactive theorem prover for first order logic.
In recent years Jussi Ketonen's (1984) EKL interactive theorem prover for
type theory has been used in a Stanford University course entitled
"Recursive programming and Proving" taught using this book.  The
availability of second order logic in EKL has proved advantageous.
The experience of proving facts about programs has the same advantages
as the study of any other mathematical domain.  Even if the student
never proves another theorem, his understanding of the subject is
enhanced by the experience.

The class experience with the interactive theorem provers has been
mixed.  Understanding is enhanced by using a fully formal system,
but debugging proofs is tedious with present systems, especially
when the computer being used is overloaded.

4 - It's not clear this insert should be made.
Small integers are sometimes represented by the number itself usually
with a certain constant added rather than by a pointer.  The constant
serves to give the representation a numerical value that can be
distinguished from the pointers into memory.  This scheme saves time
and memory space.

7 basic LISP programs. → basic LISP functions.

Sept 1

	Here's what's probably a bad idea.  Overload cons by
letting it take an arbitrary number of arguments.  The semantics
is given by (cons x y (3 4)) => (x y 3 4), which is the
same result as that given by (list x y 3 4).  The difference is
that  list  would do all the conses, using the extended cons, the
constant tail of the list is used.  Such a  cons  will make a 
good exercise in writing a macro.  Question: can we make  cons itself
into such a macro?

(DEFUN CCONS MACRO (L) 
   (OR (MACROFETCH L)
       (MACROMEMO L
		  (PROGN (SETQ L (CDR L)) (CCONS1 L))
		  'CCONS)))

(DEFUN CCONS1 (U) 
   (CONS 'CONS
	 (IF (NULL (CDDR U)) U (LIST (CAR U) (CCONS1 (CDR U))))))
* 
(grindef ccons ccons1)
(defmacro ccons l (ccons1 l))

(defun ccons1 (u)
       (cons 'cons (if (null (cddr u)) u (list (car u) (ccons1 (cdr u))))))

Sept 2 

Examples of multiple valued functions

count of re-entrant list structure

paths through graph excluding seen vertices

quick sort

The problem seems to be that to make an eval that allows multiple-valued
functions requires functions with variable numbers of values.

;;; This won't run in any present Lisp, because it uses the output
;;; of a mult-value function as two arguments of another call.  In
;;; brackets are assertions about the number of brackets.  Compiling
;;; or interpreting might be more feasible if these were included.
;;; As it stands the arguments are
;;; (u: a list of vertices to be examined)
;;; (p: the predicate that says whether a vertex wins)
;;; (found: winners already found)
;;; (seen: vertices already seen)
;;; There are two values, a list of winning vertices and a list of vertices seen

(defun wins (u p seen found)
[VAL 2 (if (null u)
	   (values found seen)
	   (wins (cdr u)
		  p
[ARGS 2		  (if (member (car u) seen)
		      (values found seen)
		      (wins (successors (car u))
			     p
			     (cons (car u) seen)
			     (if (p (car u))
				 (cons (car u) found)
				 found)))]))])

We can simplify by incorporating the test for  seen  in  successors.


(defun wins (u p seen found)
[VAL 2 (if (null u)
	   (values found seen)
	   (wins (cdr u)
		  p
[ARGS 2		  (wins (successors (car u) seen)
			 p
			 (cons (car u) seen)
			 (if (p (car u))
			     (cons (car u) found)
			     found))]))])

wins[u,p,s,f] ← if n u then f, s
		   else wins[d u, p, wins[succ[a u, s],
					  p,
					  if p a u then a u . f else f,
					  a u . s]]

section on ekl and/or Boyer-Moore

Lisp expression whose value is itself.

Pattern matcher and proof of its correctness.

Unification algorithm and proof of its correctness.

What about Jussi's higher order unifier?

comma and backquote?
Outlines:

first the outline based on abstraction first.

abstract section
internal notation, i.e. calling lisp functions and defun.